Left Termination of the query pattern
parse(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 UnifyTransformerProof (⇔, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 66 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 TRUE

(0) Obligation:

Clauses:

goal :- ','(np(S1, S2, S), verb(S2, S3, S)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), verb(S1, [], Meaning)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), ','(verb(S1, S2, Meaning), =(S2, []))).
np(Si, So, S) :- ','(det(Si, St, T), ','(noun(St, So, N), comb(T, N, S))).
comb(a, -(N, s), s(s, N, V)).
comb(the, -(N, P), s(P, N, V)).
det(.(a, S), S, a).
det(.(the, S), S, the).
noun(.(book, S), S, -(book, s)).
noun(.(books, S), S, -(book, p)).
noun(.(box, S), S, -(box, s)).
noun(.(boxes, S), S, -(box, p)).
verb(.(falls, So), So, s(s, N, fall)).
verb(.(fall, So), So, s(p, N, fall)).
verb(.(flies, So), So, s(s, N, fly)).
verb(.(fly, So), So, s(p, N, fly)).

Query: parse(g,a)

(1) UnifyTransformerProof (EQUIVALENT transformation)

Added a fact for the built-in = predicate [PROLOG].

(2) Obligation:

Clauses:

goal :- ','(np(S1, S2, S), verb(S2, S3, S)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), verb(S1, [], Meaning)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), ','(verb(S1, S2, Meaning), =(S2, []))).
np(Si, So, S) :- ','(det(Si, St, T), ','(noun(St, So, N), comb(T, N, S))).
comb(a, -(N, s), s(s, N, V)).
comb(the, -(N, P), s(P, N, V)).
det(.(a, S), S, a).
det(.(the, S), S, the).
noun(.(book, S), S, -(book, s)).
noun(.(books, S), S, -(book, p)).
noun(.(box, S), S, -(box, s)).
noun(.(boxes, S), S, -(box, p)).
verb(.(falls, So), So, s(s, N, fall)).
verb(.(fall, So), So, s(p, N, fall)).
verb(.(flies, So), So, s(s, N, fly)).
verb(.(fly, So), So, s(p, N, fly)).
=(X, X).

Query: parse(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
parse_in: (b,f)
np_in: (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

parse_in_ga(S0, Meaning) → U3_ga(S0, Meaning, np_in_gaa(S0, S1, Meaning))
np_in_gaa(Si, So, S) → U7_gaa(Si, So, S, det_in_gaa(Si, St, T))
det_in_gaa(.(a, S), S, a) → det_out_gaa(.(a, S), S, a)
det_in_gaa(.(the, S), S, the) → det_out_gaa(.(the, S), S, the)
U7_gaa(Si, So, S, det_out_gaa(Si, St, T)) → U8_gaa(Si, So, S, T, noun_in_gaa(St, So, N))
noun_in_gaa(.(book, S), S, -(book, s)) → noun_out_gaa(.(book, S), S, -(book, s))
noun_in_gaa(.(books, S), S, -(book, p)) → noun_out_gaa(.(books, S), S, -(book, p))
noun_in_gaa(.(box, S), S, -(box, s)) → noun_out_gaa(.(box, S), S, -(box, s))
noun_in_gaa(.(boxes, S), S, -(box, p)) → noun_out_gaa(.(boxes, S), S, -(box, p))
U8_gaa(Si, So, S, T, noun_out_gaa(St, So, N)) → U9_gaa(Si, So, S, comb_in_gga(T, N, S))
comb_in_gga(a, -(N, s), s(s, N, V)) → comb_out_gga(a, -(N, s), s(s, N, V))
comb_in_gga(the, -(N, P), s(P, N, V)) → comb_out_gga(the, -(N, P), s(P, N, V))
U9_gaa(Si, So, S, comb_out_gga(T, N, S)) → np_out_gaa(Si, So, S)
U3_ga(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U4_ga(S0, Meaning, verb_in_ggg(S1, [], Meaning))
verb_in_ggg(.(falls, So), So, s(s, N, fall)) → verb_out_ggg(.(falls, So), So, s(s, N, fall))
verb_in_ggg(.(fall, So), So, s(p, N, fall)) → verb_out_ggg(.(fall, So), So, s(p, N, fall))
verb_in_ggg(.(flies, So), So, s(s, N, fly)) → verb_out_ggg(.(flies, So), So, s(s, N, fly))
verb_in_ggg(.(fly, So), So, s(p, N, fly)) → verb_out_ggg(.(fly, So), So, s(p, N, fly))
U4_ga(S0, Meaning, verb_out_ggg(S1, [], Meaning)) → parse_out_ga(S0, Meaning)
U3_ga(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U5_ga(S0, Meaning, verb_in_gag(S1, S2, Meaning))
verb_in_gag(.(falls, So), So, s(s, N, fall)) → verb_out_gag(.(falls, So), So, s(s, N, fall))
verb_in_gag(.(fall, So), So, s(p, N, fall)) → verb_out_gag(.(fall, So), So, s(p, N, fall))
verb_in_gag(.(flies, So), So, s(s, N, fly)) → verb_out_gag(.(flies, So), So, s(s, N, fly))
verb_in_gag(.(fly, So), So, s(p, N, fly)) → verb_out_gag(.(fly, So), So, s(p, N, fly))
U5_ga(S0, Meaning, verb_out_gag(S1, S2, Meaning)) → U6_ga(S0, Meaning, =_in_gg(S2, []))
=_in_gg(X, X) → =_out_gg(X, X)
U6_ga(S0, Meaning, =_out_gg(S2, [])) → parse_out_ga(S0, Meaning)

The argument filtering Pi contains the following mapping:
parse_in_ga(x1, x2)  =  parse_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
np_in_gaa(x1, x2, x3)  =  np_in_gaa(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
det_in_gaa(x1, x2, x3)  =  det_in_gaa(x1)
.(x1, x2)  =  .(x1, x2)
a  =  a
det_out_gaa(x1, x2, x3)  =  det_out_gaa(x2, x3)
the  =  the
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x4, x5)
noun_in_gaa(x1, x2, x3)  =  noun_in_gaa(x1)
book  =  book
noun_out_gaa(x1, x2, x3)  =  noun_out_gaa(x2, x3)
books  =  books
box  =  box
boxes  =  boxes
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x2, x4)
comb_in_gga(x1, x2, x3)  =  comb_in_gga(x1, x2)
-(x1, x2)  =  -(x1, x2)
s  =  s
comb_out_gga(x1, x2, x3)  =  comb_out_gga(x3)
s(x1, x2, x3)  =  s(x1, x2)
np_out_gaa(x1, x2, x3)  =  np_out_gaa(x2, x3)
U4_ga(x1, x2, x3)  =  U4_ga(x2, x3)
verb_in_ggg(x1, x2, x3)  =  verb_in_ggg(x1, x2, x3)
falls  =  falls
verb_out_ggg(x1, x2, x3)  =  verb_out_ggg
fall  =  fall
p  =  p
flies  =  flies
fly  =  fly
[]  =  []
parse_out_ga(x1, x2)  =  parse_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x2, x3)
verb_in_gag(x1, x2, x3)  =  verb_in_gag(x1, x3)
verb_out_gag(x1, x2, x3)  =  verb_out_gag(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x2, x3)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

parse_in_ga(S0, Meaning) → U3_ga(S0, Meaning, np_in_gaa(S0, S1, Meaning))
np_in_gaa(Si, So, S) → U7_gaa(Si, So, S, det_in_gaa(Si, St, T))
det_in_gaa(.(a, S), S, a) → det_out_gaa(.(a, S), S, a)
det_in_gaa(.(the, S), S, the) → det_out_gaa(.(the, S), S, the)
U7_gaa(Si, So, S, det_out_gaa(Si, St, T)) → U8_gaa(Si, So, S, T, noun_in_gaa(St, So, N))
noun_in_gaa(.(book, S), S, -(book, s)) → noun_out_gaa(.(book, S), S, -(book, s))
noun_in_gaa(.(books, S), S, -(book, p)) → noun_out_gaa(.(books, S), S, -(book, p))
noun_in_gaa(.(box, S), S, -(box, s)) → noun_out_gaa(.(box, S), S, -(box, s))
noun_in_gaa(.(boxes, S), S, -(box, p)) → noun_out_gaa(.(boxes, S), S, -(box, p))
U8_gaa(Si, So, S, T, noun_out_gaa(St, So, N)) → U9_gaa(Si, So, S, comb_in_gga(T, N, S))
comb_in_gga(a, -(N, s), s(s, N, V)) → comb_out_gga(a, -(N, s), s(s, N, V))
comb_in_gga(the, -(N, P), s(P, N, V)) → comb_out_gga(the, -(N, P), s(P, N, V))
U9_gaa(Si, So, S, comb_out_gga(T, N, S)) → np_out_gaa(Si, So, S)
U3_ga(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U4_ga(S0, Meaning, verb_in_ggg(S1, [], Meaning))
verb_in_ggg(.(falls, So), So, s(s, N, fall)) → verb_out_ggg(.(falls, So), So, s(s, N, fall))
verb_in_ggg(.(fall, So), So, s(p, N, fall)) → verb_out_ggg(.(fall, So), So, s(p, N, fall))
verb_in_ggg(.(flies, So), So, s(s, N, fly)) → verb_out_ggg(.(flies, So), So, s(s, N, fly))
verb_in_ggg(.(fly, So), So, s(p, N, fly)) → verb_out_ggg(.(fly, So), So, s(p, N, fly))
U4_ga(S0, Meaning, verb_out_ggg(S1, [], Meaning)) → parse_out_ga(S0, Meaning)
U3_ga(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U5_ga(S0, Meaning, verb_in_gag(S1, S2, Meaning))
verb_in_gag(.(falls, So), So, s(s, N, fall)) → verb_out_gag(.(falls, So), So, s(s, N, fall))
verb_in_gag(.(fall, So), So, s(p, N, fall)) → verb_out_gag(.(fall, So), So, s(p, N, fall))
verb_in_gag(.(flies, So), So, s(s, N, fly)) → verb_out_gag(.(flies, So), So, s(s, N, fly))
verb_in_gag(.(fly, So), So, s(p, N, fly)) → verb_out_gag(.(fly, So), So, s(p, N, fly))
U5_ga(S0, Meaning, verb_out_gag(S1, S2, Meaning)) → U6_ga(S0, Meaning, =_in_gg(S2, []))
=_in_gg(X, X) → =_out_gg(X, X)
U6_ga(S0, Meaning, =_out_gg(S2, [])) → parse_out_ga(S0, Meaning)

The argument filtering Pi contains the following mapping:
parse_in_ga(x1, x2)  =  parse_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
np_in_gaa(x1, x2, x3)  =  np_in_gaa(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
det_in_gaa(x1, x2, x3)  =  det_in_gaa(x1)
.(x1, x2)  =  .(x1, x2)
a  =  a
det_out_gaa(x1, x2, x3)  =  det_out_gaa(x2, x3)
the  =  the
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x4, x5)
noun_in_gaa(x1, x2, x3)  =  noun_in_gaa(x1)
book  =  book
noun_out_gaa(x1, x2, x3)  =  noun_out_gaa(x2, x3)
books  =  books
box  =  box
boxes  =  boxes
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x2, x4)
comb_in_gga(x1, x2, x3)  =  comb_in_gga(x1, x2)
-(x1, x2)  =  -(x1, x2)
s  =  s
comb_out_gga(x1, x2, x3)  =  comb_out_gga(x3)
s(x1, x2, x3)  =  s(x1, x2)
np_out_gaa(x1, x2, x3)  =  np_out_gaa(x2, x3)
U4_ga(x1, x2, x3)  =  U4_ga(x2, x3)
verb_in_ggg(x1, x2, x3)  =  verb_in_ggg(x1, x2, x3)
falls  =  falls
verb_out_ggg(x1, x2, x3)  =  verb_out_ggg
fall  =  fall
p  =  p
flies  =  flies
fly  =  fly
[]  =  []
parse_out_ga(x1, x2)  =  parse_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x2, x3)
verb_in_gag(x1, x2, x3)  =  verb_in_gag(x1, x3)
verb_out_gag(x1, x2, x3)  =  verb_out_gag(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x2, x3)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

PARSE_IN_GA(S0, Meaning) → U3_GA(S0, Meaning, np_in_gaa(S0, S1, Meaning))
PARSE_IN_GA(S0, Meaning) → NP_IN_GAA(S0, S1, Meaning)
NP_IN_GAA(Si, So, S) → U7_GAA(Si, So, S, det_in_gaa(Si, St, T))
NP_IN_GAA(Si, So, S) → DET_IN_GAA(Si, St, T)
U7_GAA(Si, So, S, det_out_gaa(Si, St, T)) → U8_GAA(Si, So, S, T, noun_in_gaa(St, So, N))
U7_GAA(Si, So, S, det_out_gaa(Si, St, T)) → NOUN_IN_GAA(St, So, N)
U8_GAA(Si, So, S, T, noun_out_gaa(St, So, N)) → U9_GAA(Si, So, S, comb_in_gga(T, N, S))
U8_GAA(Si, So, S, T, noun_out_gaa(St, So, N)) → COMB_IN_GGA(T, N, S)
U3_GA(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U4_GA(S0, Meaning, verb_in_ggg(S1, [], Meaning))
U3_GA(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → VERB_IN_GGG(S1, [], Meaning)
U3_GA(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U5_GA(S0, Meaning, verb_in_gag(S1, S2, Meaning))
U3_GA(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → VERB_IN_GAG(S1, S2, Meaning)
U5_GA(S0, Meaning, verb_out_gag(S1, S2, Meaning)) → U6_GA(S0, Meaning, =_in_gg(S2, []))
U5_GA(S0, Meaning, verb_out_gag(S1, S2, Meaning)) → =_IN_GG(S2, [])

The TRS R consists of the following rules:

parse_in_ga(S0, Meaning) → U3_ga(S0, Meaning, np_in_gaa(S0, S1, Meaning))
np_in_gaa(Si, So, S) → U7_gaa(Si, So, S, det_in_gaa(Si, St, T))
det_in_gaa(.(a, S), S, a) → det_out_gaa(.(a, S), S, a)
det_in_gaa(.(the, S), S, the) → det_out_gaa(.(the, S), S, the)
U7_gaa(Si, So, S, det_out_gaa(Si, St, T)) → U8_gaa(Si, So, S, T, noun_in_gaa(St, So, N))
noun_in_gaa(.(book, S), S, -(book, s)) → noun_out_gaa(.(book, S), S, -(book, s))
noun_in_gaa(.(books, S), S, -(book, p)) → noun_out_gaa(.(books, S), S, -(book, p))
noun_in_gaa(.(box, S), S, -(box, s)) → noun_out_gaa(.(box, S), S, -(box, s))
noun_in_gaa(.(boxes, S), S, -(box, p)) → noun_out_gaa(.(boxes, S), S, -(box, p))
U8_gaa(Si, So, S, T, noun_out_gaa(St, So, N)) → U9_gaa(Si, So, S, comb_in_gga(T, N, S))
comb_in_gga(a, -(N, s), s(s, N, V)) → comb_out_gga(a, -(N, s), s(s, N, V))
comb_in_gga(the, -(N, P), s(P, N, V)) → comb_out_gga(the, -(N, P), s(P, N, V))
U9_gaa(Si, So, S, comb_out_gga(T, N, S)) → np_out_gaa(Si, So, S)
U3_ga(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U4_ga(S0, Meaning, verb_in_ggg(S1, [], Meaning))
verb_in_ggg(.(falls, So), So, s(s, N, fall)) → verb_out_ggg(.(falls, So), So, s(s, N, fall))
verb_in_ggg(.(fall, So), So, s(p, N, fall)) → verb_out_ggg(.(fall, So), So, s(p, N, fall))
verb_in_ggg(.(flies, So), So, s(s, N, fly)) → verb_out_ggg(.(flies, So), So, s(s, N, fly))
verb_in_ggg(.(fly, So), So, s(p, N, fly)) → verb_out_ggg(.(fly, So), So, s(p, N, fly))
U4_ga(S0, Meaning, verb_out_ggg(S1, [], Meaning)) → parse_out_ga(S0, Meaning)
U3_ga(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U5_ga(S0, Meaning, verb_in_gag(S1, S2, Meaning))
verb_in_gag(.(falls, So), So, s(s, N, fall)) → verb_out_gag(.(falls, So), So, s(s, N, fall))
verb_in_gag(.(fall, So), So, s(p, N, fall)) → verb_out_gag(.(fall, So), So, s(p, N, fall))
verb_in_gag(.(flies, So), So, s(s, N, fly)) → verb_out_gag(.(flies, So), So, s(s, N, fly))
verb_in_gag(.(fly, So), So, s(p, N, fly)) → verb_out_gag(.(fly, So), So, s(p, N, fly))
U5_ga(S0, Meaning, verb_out_gag(S1, S2, Meaning)) → U6_ga(S0, Meaning, =_in_gg(S2, []))
=_in_gg(X, X) → =_out_gg(X, X)
U6_ga(S0, Meaning, =_out_gg(S2, [])) → parse_out_ga(S0, Meaning)

The argument filtering Pi contains the following mapping:
parse_in_ga(x1, x2)  =  parse_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
np_in_gaa(x1, x2, x3)  =  np_in_gaa(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
det_in_gaa(x1, x2, x3)  =  det_in_gaa(x1)
.(x1, x2)  =  .(x1, x2)
a  =  a
det_out_gaa(x1, x2, x3)  =  det_out_gaa(x2, x3)
the  =  the
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x4, x5)
noun_in_gaa(x1, x2, x3)  =  noun_in_gaa(x1)
book  =  book
noun_out_gaa(x1, x2, x3)  =  noun_out_gaa(x2, x3)
books  =  books
box  =  box
boxes  =  boxes
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x2, x4)
comb_in_gga(x1, x2, x3)  =  comb_in_gga(x1, x2)
-(x1, x2)  =  -(x1, x2)
s  =  s
comb_out_gga(x1, x2, x3)  =  comb_out_gga(x3)
s(x1, x2, x3)  =  s(x1, x2)
np_out_gaa(x1, x2, x3)  =  np_out_gaa(x2, x3)
U4_ga(x1, x2, x3)  =  U4_ga(x2, x3)
verb_in_ggg(x1, x2, x3)  =  verb_in_ggg(x1, x2, x3)
falls  =  falls
verb_out_ggg(x1, x2, x3)  =  verb_out_ggg
fall  =  fall
p  =  p
flies  =  flies
fly  =  fly
[]  =  []
parse_out_ga(x1, x2)  =  parse_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x2, x3)
verb_in_gag(x1, x2, x3)  =  verb_in_gag(x1, x3)
verb_out_gag(x1, x2, x3)  =  verb_out_gag(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x2, x3)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
PARSE_IN_GA(x1, x2)  =  PARSE_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
NP_IN_GAA(x1, x2, x3)  =  NP_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x4)
DET_IN_GAA(x1, x2, x3)  =  DET_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x4, x5)
NOUN_IN_GAA(x1, x2, x3)  =  NOUN_IN_GAA(x1)
U9_GAA(x1, x2, x3, x4)  =  U9_GAA(x2, x4)
COMB_IN_GGA(x1, x2, x3)  =  COMB_IN_GGA(x1, x2)
U4_GA(x1, x2, x3)  =  U4_GA(x2, x3)
VERB_IN_GGG(x1, x2, x3)  =  VERB_IN_GGG(x1, x2, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x2, x3)
VERB_IN_GAG(x1, x2, x3)  =  VERB_IN_GAG(x1, x3)
U6_GA(x1, x2, x3)  =  U6_GA(x2, x3)
=_IN_GG(x1, x2)  =  =_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PARSE_IN_GA(S0, Meaning) → U3_GA(S0, Meaning, np_in_gaa(S0, S1, Meaning))
PARSE_IN_GA(S0, Meaning) → NP_IN_GAA(S0, S1, Meaning)
NP_IN_GAA(Si, So, S) → U7_GAA(Si, So, S, det_in_gaa(Si, St, T))
NP_IN_GAA(Si, So, S) → DET_IN_GAA(Si, St, T)
U7_GAA(Si, So, S, det_out_gaa(Si, St, T)) → U8_GAA(Si, So, S, T, noun_in_gaa(St, So, N))
U7_GAA(Si, So, S, det_out_gaa(Si, St, T)) → NOUN_IN_GAA(St, So, N)
U8_GAA(Si, So, S, T, noun_out_gaa(St, So, N)) → U9_GAA(Si, So, S, comb_in_gga(T, N, S))
U8_GAA(Si, So, S, T, noun_out_gaa(St, So, N)) → COMB_IN_GGA(T, N, S)
U3_GA(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U4_GA(S0, Meaning, verb_in_ggg(S1, [], Meaning))
U3_GA(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → VERB_IN_GGG(S1, [], Meaning)
U3_GA(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U5_GA(S0, Meaning, verb_in_gag(S1, S2, Meaning))
U3_GA(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → VERB_IN_GAG(S1, S2, Meaning)
U5_GA(S0, Meaning, verb_out_gag(S1, S2, Meaning)) → U6_GA(S0, Meaning, =_in_gg(S2, []))
U5_GA(S0, Meaning, verb_out_gag(S1, S2, Meaning)) → =_IN_GG(S2, [])

The TRS R consists of the following rules:

parse_in_ga(S0, Meaning) → U3_ga(S0, Meaning, np_in_gaa(S0, S1, Meaning))
np_in_gaa(Si, So, S) → U7_gaa(Si, So, S, det_in_gaa(Si, St, T))
det_in_gaa(.(a, S), S, a) → det_out_gaa(.(a, S), S, a)
det_in_gaa(.(the, S), S, the) → det_out_gaa(.(the, S), S, the)
U7_gaa(Si, So, S, det_out_gaa(Si, St, T)) → U8_gaa(Si, So, S, T, noun_in_gaa(St, So, N))
noun_in_gaa(.(book, S), S, -(book, s)) → noun_out_gaa(.(book, S), S, -(book, s))
noun_in_gaa(.(books, S), S, -(book, p)) → noun_out_gaa(.(books, S), S, -(book, p))
noun_in_gaa(.(box, S), S, -(box, s)) → noun_out_gaa(.(box, S), S, -(box, s))
noun_in_gaa(.(boxes, S), S, -(box, p)) → noun_out_gaa(.(boxes, S), S, -(box, p))
U8_gaa(Si, So, S, T, noun_out_gaa(St, So, N)) → U9_gaa(Si, So, S, comb_in_gga(T, N, S))
comb_in_gga(a, -(N, s), s(s, N, V)) → comb_out_gga(a, -(N, s), s(s, N, V))
comb_in_gga(the, -(N, P), s(P, N, V)) → comb_out_gga(the, -(N, P), s(P, N, V))
U9_gaa(Si, So, S, comb_out_gga(T, N, S)) → np_out_gaa(Si, So, S)
U3_ga(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U4_ga(S0, Meaning, verb_in_ggg(S1, [], Meaning))
verb_in_ggg(.(falls, So), So, s(s, N, fall)) → verb_out_ggg(.(falls, So), So, s(s, N, fall))
verb_in_ggg(.(fall, So), So, s(p, N, fall)) → verb_out_ggg(.(fall, So), So, s(p, N, fall))
verb_in_ggg(.(flies, So), So, s(s, N, fly)) → verb_out_ggg(.(flies, So), So, s(s, N, fly))
verb_in_ggg(.(fly, So), So, s(p, N, fly)) → verb_out_ggg(.(fly, So), So, s(p, N, fly))
U4_ga(S0, Meaning, verb_out_ggg(S1, [], Meaning)) → parse_out_ga(S0, Meaning)
U3_ga(S0, Meaning, np_out_gaa(S0, S1, Meaning)) → U5_ga(S0, Meaning, verb_in_gag(S1, S2, Meaning))
verb_in_gag(.(falls, So), So, s(s, N, fall)) → verb_out_gag(.(falls, So), So, s(s, N, fall))
verb_in_gag(.(fall, So), So, s(p, N, fall)) → verb_out_gag(.(fall, So), So, s(p, N, fall))
verb_in_gag(.(flies, So), So, s(s, N, fly)) → verb_out_gag(.(flies, So), So, s(s, N, fly))
verb_in_gag(.(fly, So), So, s(p, N, fly)) → verb_out_gag(.(fly, So), So, s(p, N, fly))
U5_ga(S0, Meaning, verb_out_gag(S1, S2, Meaning)) → U6_ga(S0, Meaning, =_in_gg(S2, []))
=_in_gg(X, X) → =_out_gg(X, X)
U6_ga(S0, Meaning, =_out_gg(S2, [])) → parse_out_ga(S0, Meaning)

The argument filtering Pi contains the following mapping:
parse_in_ga(x1, x2)  =  parse_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
np_in_gaa(x1, x2, x3)  =  np_in_gaa(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
det_in_gaa(x1, x2, x3)  =  det_in_gaa(x1)
.(x1, x2)  =  .(x1, x2)
a  =  a
det_out_gaa(x1, x2, x3)  =  det_out_gaa(x2, x3)
the  =  the
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x4, x5)
noun_in_gaa(x1, x2, x3)  =  noun_in_gaa(x1)
book  =  book
noun_out_gaa(x1, x2, x3)  =  noun_out_gaa(x2, x3)
books  =  books
box  =  box
boxes  =  boxes
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x2, x4)
comb_in_gga(x1, x2, x3)  =  comb_in_gga(x1, x2)
-(x1, x2)  =  -(x1, x2)
s  =  s
comb_out_gga(x1, x2, x3)  =  comb_out_gga(x3)
s(x1, x2, x3)  =  s(x1, x2)
np_out_gaa(x1, x2, x3)  =  np_out_gaa(x2, x3)
U4_ga(x1, x2, x3)  =  U4_ga(x2, x3)
verb_in_ggg(x1, x2, x3)  =  verb_in_ggg(x1, x2, x3)
falls  =  falls
verb_out_ggg(x1, x2, x3)  =  verb_out_ggg
fall  =  fall
p  =  p
flies  =  flies
fly  =  fly
[]  =  []
parse_out_ga(x1, x2)  =  parse_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x2, x3)
verb_in_gag(x1, x2, x3)  =  verb_in_gag(x1, x3)
verb_out_gag(x1, x2, x3)  =  verb_out_gag(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x2, x3)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
PARSE_IN_GA(x1, x2)  =  PARSE_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
NP_IN_GAA(x1, x2, x3)  =  NP_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x4)
DET_IN_GAA(x1, x2, x3)  =  DET_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x4, x5)
NOUN_IN_GAA(x1, x2, x3)  =  NOUN_IN_GAA(x1)
U9_GAA(x1, x2, x3, x4)  =  U9_GAA(x2, x4)
COMB_IN_GGA(x1, x2, x3)  =  COMB_IN_GGA(x1, x2)
U4_GA(x1, x2, x3)  =  U4_GA(x2, x3)
VERB_IN_GGG(x1, x2, x3)  =  VERB_IN_GGG(x1, x2, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x2, x3)
VERB_IN_GAG(x1, x2, x3)  =  VERB_IN_GAG(x1, x3)
U6_GA(x1, x2, x3)  =  U6_GA(x2, x3)
=_IN_GG(x1, x2)  =  =_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 14 less nodes.

(8) TRUE